es:event_system{i:l}. 
es_val(es)  e:es-E(es)kindcase(es-kind(es; e); a.(es-V(es)(loc(e),a)); l,t.(es-M(es)(l,t))) 

latex

Definitions	t  T, es_info(es), es_val(es), es-M(es), loc(e), es-V(es), es-kind(es; e), es-E(es), x:A  B(x), event_system{i:l}, x:AB(x), Type, f(a), kindcase(k; a.f(a); l,t.g(l;t)), x:A. B(x)
Lemmas	event system wf